\begin{tabbing}
EventsWithValues
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$E$:Type\+
\\[0ex]$\times$ (${\it eq}$:EqDecider($E$)
\\[0ex]$\times$ ${\it pred?}$:($E$$\rightarrow$(?$E$))
\\[0ex]$\times$ ${\it info}$:($E$$\rightarrow$((:Id $\times$ Id) + (:(:IdLnk $\times$ $E$) $\times$ Id)))
\\[0ex]$\times$ ${\it oaxioms}$:EOrderAxioms($E$; ${\it pred?}$; ${\it info}$)
\\[0ex]$\times$ $T$:(Id$\rightarrow$Id$\rightarrow$Type)
\\[0ex]$\times$ ${\it when}$:($x$:Id$\rightarrow$$e$:$E$$\rightarrow$$T$(loc($e$),$x$))
\\[0ex]$\times$ ${\it after}$:($x$:Id$\rightarrow$$e$:$E$$\rightarrow$$T$(loc($e$),$x$))
\\[0ex]$\times$ ${\it saxiom}$:($\forall$$e$:$E$. ($\neg$($\uparrow$first($e$))) $\Rightarrow$ ($\forall$$x$:Id. ${\it when}$($x$,$e$) = ${\it after}$($x$,pred($e$))))
\\[0ex]$\times$ $V$:(Knd$\rightarrow$Id$\rightarrow$Type)
\\[0ex]$\times$ (${\it val}$:($e$:$E$$\rightarrow$$V$(kind($e$),loc($e$)))
\\[0ex]$\times$ Top))
\-
\end{tabbing}